Symposium `Logica in de lage landen'

VvL symposium. Vrijdag 12 november 2004 in zaal 414 van de de Jaarbeurs in Utrecht.

Programma:
[12.45-13.30] Broodjeslunch annex VvL algemene ledenvergadering
[13.30-14.15] Dirk van Dalen, "Wat dacht Brouwer van de logica?"
[14.15-14.30] koffie- en theepauze
[14.30-15.15] Gerard Alberts, "Van Wijngaarden en logica: een gemiste verbinding"
[15.15-15.30] koffie- en theepauze
[15.30-16.15] Rob Nederpelt, "Automath"
[16.15-17.00] borrel


Abstracts

Dirk van Dalen
Er zijn nauwelijks gegevens over Brouwers opvattingen waar het de logica betreft. In de correspondentie met Korteweg komen wat provocerende opinies voor, maar die kunnen niet als maatgevend beschouwd worden. De dissertatie geeft hier en daar wat commentaar op de logica, en verder kunnen we alleen afgaan op ``logica in gebruik". Niettemin is het lonend om nader op de schaarse gegevens in te gaan.

Gerard Alberts
Vanaf het allereerste begin van computers is de verbinding gelegd tussen denken en computers (Von Neumann, Wiener, Turing). De achtergrond van mathematische logica bij het denken over berekenbaarheid (Post, Church, Turing) is door Martin Davis goed beschreven. Er wordt rond 1950 druk geconfereerd over rekenmachines als toegepaste logica (vanuit Nederland heeft Freudenthal zich daarmee bemoeid). Dat blijft allemaal bij abstracte speculaties, met de feitelijke bouw van rekenautomaten en programmeren heeft dat nog vrijwel niets te maken.
Serieus werd het in de jaren zestig toen men echt probeerde logica toe te passen op het ontwerp van programmeertalen en later op vraagstukken van programmacorrectheid.
Mijn bijdrage is gecentreerd rond Van Wijngaardens opstel ``Generalized Algol'' uit 1962 waarmee hij een schot voor de boeg gaf aan zijn collega's in het nadenken over een opvolger van ALGOL 60. Het gebeurde in Rome op de conferentie waar de basis werd gelegd voor WG 2.1, de IFIP-werkgroep waarbinnen Van Wijngaarden zijn belangrijkste invloed zou uitoefenen. De voordracht was wonderlijk omdat hij heel ver ging in de abstractie van het idee van programmeertaal. De voordracht was nog wonderlijker omdat hij duidelijk vroeg om logica (en noties van syntax en semantiek) en tegelijk liet zien dat Van Wijngaarden daarmee niet vertrouwd was: een gemiste verbinding.

Rob Nederpelt
Around 1967, the well-known Dutch mathematician N.G. de Bruijn developed a formal language for mathematics, which he baptized `Automath', since he wanted to Automate Mathematics. In the language Automath he included essential aspects of mathematics like definitions and proofs, which up to that day were mainly treated as being meta-mathematical. His aim was that the logical framework present in Automath would be strong enough not only for expressing mathematical content, but also for its (automatic) verification. For the latter purpose he wanted to call in the computer, which in that time only just had started its triumphal progress.
De Bruijn succeeded in designing a powerful and elegant formal language, suitable for his purposes. It was immediately implemented on a machine and tested with a large corpus of mathematical texts, taken from various fields and with complexity ranging from introductory to very advanced.
In the talk I first sketch the history of the Automath project. Next, I discuss some basic innovations first introduced in this formal language, in particular the well-organized (line-by-line) definitional structure and the influential `propositions-as-types' notion. Finally, I describe the connections of Automath with modern type systems such as the ones coined by Henk Barendregt.